Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta) by mitschabaude-bot · Pull Request #274 · Verified-zkEVM/CompPoly

mitschabaude-bot · 2026-07-25T09:39:48Z

Summary

This PR is now rebased onto main and contains only the work that remains after the shared eight-limb Montgomery stack landed in #284.

Add canonical Pallas and Vesta base fields, including kernel-checked Pratt primality certificates and the Pasta 2-cycle aliases.
Instantiate both fields over the existing Montgomery.Native64x8.FastField implementation, with the standard ofField and ringEquiv API.
Add regression coverage for raw Montgomery operations, both concrete field instances, inversion, powers, and canonical-field agreement.
Add Montgomery/ScalarFft.lean, an in-place radix-2 DIT FFT over eight-limb Montgomery residues and precomputed twiddles.

Runtime layout

ScalarFft imports only Native64x8Defs. This keeps its full precompileModules import closure free of Mathlib, matching the downstream Ironwood verifier-key certificate that uses this arithmetic for its MSM and FFT. The FFT module currently contains runtime definitions only; its correctness proof remains downstream until it is upstreamed separately.

Validation

lake build
lake test
./scripts/check-imports.sh
./scripts/lint-style.sh
python3 ./scripts/check-docs-integrity.py

All required CI checks are green.

github-actions · 2026-07-25T09:43:59Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)

Proven eight-limb Montgomery field arithmetic for 255-bit moduli, instantiated on the Pasta curves (Pallas/Vesta), with a zero-import runtime definitions module for native compilation. The PR also refactors the existing BabyBear and KoalaBear fast field implementations to use a shared 32-bit Montgomery library, consolidates NTT domain structures, and updates documentation and benchmarks. No new sorrys or admits are introduced.

Statistics

Metric	Count
📝 Files Changed	30
✅ Lines Added	3548
❌ Lines Removed	1690

Lean Declarations

✏️ Removed: 150 declaration(s)

CompPoly/Fields/BabyBear.lean (21)

@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) :
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
abbrev Field
def fieldSize : Nat
def pBits : Nat
def twoAdicGenerators : List Field
def twoAdicity : Nat
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) :
lemma twoAdicGenerator_unit_mem_rootsOfUnity
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1)
private def sqChain (g : Field) : Nat → Field
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) :
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28)
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) :
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) :
theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/KoalaBear/Fast.lean (121)

@[simp] theorem modulus64_toNat : modulus64.toNat = KoalaBear.fieldSize
@[simp] theorem modulus_toNat : modulus.toNat = KoalaBear.fieldSize
def add (x y : Field) : Field
def div (x y : Field) : Field
def inv (x : Field) : Field
def invExponent : Nat
def modulus : UInt32
def modulus64 : UInt64
def montgomeryNegInv : UInt32
def montgomeryReduce (x : UInt64) : Field
def mul (x y : Field) : Field
def neg (x : Field) : Field
def ofCanonicalNat (n : Nat) (_h : n < KoalaBear.fieldSize) : Field
def ofInt (n : Int) : Field
def ofNat (n : Nat) : Field
def one : Field
def pow (x : Field) (n : Nat) : Field
def r2ModModulus : UInt32
def rModModulus : UInt32
def raw (x : Field) : UInt32
def reduceUInt64 (x : UInt64) : Field
def square (x : Field) : Field
def sub (x y : Field) : Field
def toCanonicalUInt32 (x : Field) : UInt32
def toField (x : Field) : KoalaBear.Field
def toNat (x : Field) : Nat
def zero : Field
instance instAddField : Add Field where
instance instDivField : Div Field where
instance instIntCastField : IntCast Field where
instance instIntSMulField : SMul Int Field where
instance instInvField : Inv Field where
instance instMulField : Mul Field where
instance instNNRatCastField : NNRatCast Field where
instance instNNRatSMulField : SMul ℚ≥0 Field where
instance instNatCastField : NatCast Field where
instance instNatSMulField : SMul Nat Field where
instance instNegField : Neg Field where
instance instOneField : One Field where
instance instPowFieldInt : Pow Field Int where
instance instPowFieldNat : Pow Field Nat where
instance instRatCastField : RatCast Field where
instance instRatSMulField : SMul ℚ Field where
instance instSubField : Sub Field where
instance instZeroField : Zero Field where
private def montgomeryReduceBounded (x : UInt64)
private def montgomeryReduceBoundedRaw (x : UInt64) : UInt32
private def montgomeryReduceNat (x : Nat) : Nat
private def reduceUInt32 (x : UInt32) : Field
private def reduceUInt32Lt2Modulus (x : UInt32) (h : x.toNat < 2 * KoalaBear.fieldSize) :
private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
private def shift4Mul (acc digit : Field) : Field
private theorem fieldSize_add_fieldSize_lt_two64 :
private theorem fieldSize_add_fieldSize_lt_uint32Size :
private theorem fieldSize_lt_uint32Size : KoalaBear.fieldSize < UInt32.size
private theorem fieldSize_mul_fieldSize_lt_two64 :
private theorem fieldSize_mul_uint32Size_lt_two64 :
private theorem fieldSize_pos : 0 < KoalaBear.fieldSize
private theorem montgomeryQuotient_cast (x : Nat) :
private theorem montgomeryReduceBoundedRaw_lt (x : UInt64)
private theorem montgomeryReduceBounded_cast (x : UInt64)
private theorem montgomeryReduceNat_cast (x : Nat) :
private theorem montgomeryReduceNat_lt (x : Nat)
private theorem montgomery_sum_dvd (x : Nat) :
private theorem montgomery_u_eq_nat (x : UInt64)
private theorem montgomery_u_lt_two_fieldSize (x : UInt64)
private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
private theorem nat_eq_of_field_eq {a b : Nat} (ha : a < KoalaBear.fieldSize)
private theorem ofCanonicalNat_raw_cast (n : Nat) (h : n < KoalaBear.fieldSize) :
private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
private theorem r2ModModulus_cast :
private theorem r2ModModulus_lt_fieldSize : r2ModModulus.toNat < KoalaBear.fieldSize
private theorem rModModulus_cast :
private theorem rModModulus_lt_fieldSize : rModModulus.toNat < KoalaBear.fieldSize
private theorem raw_cast_eq_toField_mul (x : Field) :
private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
private theorem reduceUInt32Lt2Modulus_val_eq_nat (x : UInt32)
private theorem reduceUInt64_raw_cast (x : UInt64) :
private theorem toField_div_mul_inv (x y : Field) :
private theorem toField_eq_raw_mul_inv (x : Field) :
private theorem toField_inv_pow (x : Field) :
private theorem toField_inv_raw (x : Field) : toField (inv x) = (toField x)⁻¹
private theorem toField_mul_pow (base x y : Field) (m n : Nat)
private theorem toField_mul_raw (x y : Field) : toField (mul x y) = toField x * toField y
private theorem toField_ofCanonicalNat_aux (n : Nat) (h : n < KoalaBear.fieldSize) :
private theorem toField_shift4Mul (acc digit : Field) :
private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
private theorem toNat_lt_fieldSize (x : Field) : toNat x < KoalaBear.fieldSize
private theorem two_fieldSize_mul_uint32Size_lt_two64 :
private theorem uint32Size_lt_three_fieldSize :
private theorem uint32Size_ne_zero_in_field :
theorem ofField_toField (x : Field) : ofField (toField x) = x
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
theorem ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x
theorem toField_add (x y : Field) : toField (x + y) = toField x + toField y
theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
theorem toField_injective : Function.Injective toField
theorem toField_intCast (n : Int) : toField (n : Field) = (n : KoalaBear.Field)
theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
theorem toField_natCast (n : Nat) : toField (n : Field) = (n : KoalaBear.Field)
theorem toField_neg (x : Field) : toField (-x) = -toField x
theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x
theorem toField_nnratCast (q : ℚ≥0) : toField (q : Field) = (q : KoalaBear.Field)
theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n
theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x
theorem toField_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) :
theorem toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x
theorem toField_one : toField (1 : Field) = 1
theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n
theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x
theorem toField_ratCast (q : ℚ) : toField (q : Field) = (q : KoalaBear.Field)
theorem toField_reduceUInt64 (x : UInt64) :
theorem toField_square (x : Field) : toField (square x) = toField x * toField x
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : Field) = 0
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
theorem toNat_ofCanonicalNat (n : Nat) (h : n < KoalaBear.fieldSize) :
theorem toNat_reduceUInt64 (x : UInt64) :

CompPoly/Univariate/NTT/BabyBear.lean (1)

theorem twoPowNatCast_ne_zero

CompPoly/Univariate/NTT/KoalaBear.lean (3)

theorem fast_isPrimitiveRoot_twoAdicGenerator
theorem fast_twoPowNatCast_ne_zero
theorem twoPowNatCast_ne_zero

bench/CompPolyBench/Univariate/Common.lean (4)

def koalaBearFastDomainOfLogN (logN : Nat) (hlogN : logN ≤ KoalaBear.twoAdicity) :
noncomputable def koalaBearFastRingEquiv : KoalaBear.Fast.Field ≃+* KoalaBear.Field where
theorem koalaBearFast_isPrimitiveRoot_twoAdicGenerator
theorem koalaBearFast_twoPowNatCast_ne_zero

✏️ Added: 320 declaration(s)

CompPoly/Fields/BabyBear/Basic.lean (22)

@[simp] lemma twoAdicGenerators_length : twoAdicGenerators.length = twoAdicity + 1
@[simp] lemma twoAdicGenerators_succ_square_eq (idx : Nat) (h : idx < twoAdicity) :
@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
abbrev Field
def fieldSize : Nat
def pBits : Nat
def twoAdicGenerators : List Field
def twoAdicity : Nat
lemma fieldSize_sub_one_factorization : fieldSize - 1 = 2 ^ twoAdicity * 15
lemma inv_eq_pow (a : Field) (ha : a ≠ 0) : a⁻¹ = a ^ (fieldSize - 2)
lemma isPrimitiveRoot_twoAdicGenerator (n : Fin (twoAdicity + 1)) :
lemma twoAdicGenerator_unit_mem_rootsOfUnity
lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_eq_one (bits : Fin (twoAdicity + 1)) :
lemma twoAdicGenerators_pow_twoPow_ne_one_of_lt
lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1)
private def sqChain (g : Field) : Nat → Field
private lemma twoAdicGenerators_ne_one_of_pos (n : Fin (twoAdicity + 1)) (hn : 0 < n) :
private lemma twoAdicGenerators_pow_ne_one_aux (n : Fin 28) (m : Fin 28)
private theorem sqChain_eq_pow_two_pow (g : Field) (n : Nat) :
private theorem sqChain_twoAdicGenerators_shift (k n : Nat) (hkn : k + n ≤ twoAdicity) :
theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/BabyBear/Fast.lean (5)

abbrev Field : Type
def ofField (x : BabyBear.Field) : Field
def ofUInt32 (x : UInt32) : Field
def ringEquiv : Field ≃+* BabyBear.Field
instance instMont32Field : Mont32Field BabyBear.fieldSize where

CompPoly/Fields/KoalaBear/Fast.lean (3)

def twoAdicGenerators : List Field
instance instMont32Field : Mont32Field KoalaBear.fieldSize where
theorem twoAdicGenerators_eq_map :

CompPoly/Fields/Montgomery/Basic.lean (8)

def reduceNat (R p negInv x : ℕ) : ℕ
def reduceNatQuotient (R p negInv x : ℕ) : ℕ
theorem dvd_add (R p negInv : ℕ) (hR : 0 < R)
theorem natCast_inj_of_lt {p a b : ℕ} (h : (a : ZMod p) = (b : ZMod p))
theorem reduceNatQuotient_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R)
theorem reduceNatQuotient_lt_two_mul (R p negInv x : ℕ)
theorem reduceNat_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R)
theorem reduceNat_lt (R p negInv x : ℕ)

CompPoly/Fields/Montgomery/Native32.lean (11)

def conditionalSubtract (p32 : UInt32) (u : UInt32) : UInt32
def reduceQuotient (negInv : UInt32) (p x : UInt64) : UInt32
def reduceRaw (p32 : UInt32) (p64 : UInt64) (negInv : UInt32) (x : UInt64) : UInt32
theorem conditionalSubtract_cast :
theorem conditionalSubtract_lt (h : u.toNat < 2 * p32.toNat) :
theorem conditionalSubtract_toNat :
theorem reduceQuotient_toNat (hp_pos : 0 < p64.toNat) (hbound : p64.toNat < 2 ^ 31)
theorem reduceRaw_cast [Fact (Nat.Prime modulus)]
theorem reduceRaw_eq_conditionalSubtract :
theorem reduceRaw_lt (hp : p32.toNat = p64.toNat) (hp_pos : 0 < p64.toNat)
theorem reduceRaw_toNat (hp32 : p32.toNat = modulus) (hp64 : p64.toNat = modulus)

CompPoly/Fields/Montgomery/Native32Field.lean (79)

@[simp] theorem modulus32_lt_two_pow_31 : P.modulus32.toNat < 2 ^ 31
@[simp] theorem modulus32_pos : 0 < P.modulus32.toNat
@[simp] theorem modulus64_lt_two_pow_31 : P.modulus64.toNat < 2 ^ 31
@[simp] theorem modulus64_pos : 0 < P.modulus64.toNat
@[simp] theorem modulus_lt_two_pow_32 : modulus < 2 ^ 32
def FastField (modulus : ℕ) [Mont32Field modulus] : Type
def add (x y : FastField modulus) : FastField modulus
def div (x y : FastField modulus) : FastField modulus
def inv (x : FastField modulus) : FastField modulus
def mul (x y : FastField modulus) : FastField modulus
def neg (x : FastField modulus) : FastField modulus
def ofCanonicalNat (n : ℕ) (h : n < modulus) : FastField modulus
def ofField (x : ZMod modulus) : FastField modulus
def ofNat (modulus : ℕ) [P : Mont32Field modulus] (n : ℕ) : FastField modulus
def ofUInt32 (modulus : ℕ) [P : Mont32Field modulus] (x : UInt32) : FastField modulus
def one (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus
def pow (x : FastField modulus) (n : ℕ) : FastField modulus
def reduce (x : UInt64) (h : x.toNat < modulus * 2 ^ 32) : FastField modulus
def ringEquiv (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus ≃+* ZMod modulus where
def square (x : FastField modulus) : FastField modulus
def sub (x y : FastField modulus) : FastField modulus
def toField (x : FastField modulus) : ZMod modulus
def toNat (x : FastField modulus) : ℕ
def toUInt32 (x : FastField modulus) : UInt32
def zero (modulus : ℕ) [P : Mont32Field modulus] : FastField modulus
instance instField : _root_.Field (FastField modulus)
instance instNonBinaryField : NonBinaryField (FastField modulus) where
private def ofInt (modulus : ℕ) [P : Mont32Field modulus] (n : Int) : FastField modulus
private theorem inv_eq_pow {a : ZMod modulus} (ha : a ≠ 0) :
private theorem mul_assoc (x y z : FastField modulus) : (x * y) * z = x * (y * z)
private theorem mul_val_toNat_cast (x y : FastField modulus) :
private theorem ofCanonicalNat_val_toNat_cast {n : ℕ} (h : n < modulus) :
private theorem pow_succ_field (x : FastField modulus) (n : ℕ) : pow x (n + 1) = pow x n * x
private theorem reduce_val_toNat_cast {x : UInt64}
private theorem toField_eq_val_toNat_cast_mul_inv {x : FastField modulus} :
private theorem val_toNat_cast_eq_toField_mul {x : FastField modulus} :
theorem FastField.val_toNat_lt (x : FastField modulus) : x.val.toNat < modulus
theorem add_def (x y : FastField modulus) : x + y = add x y
theorem div_def (x y : FastField modulus) : x / y = x * y⁻¹
theorem inv_def (x : FastField modulus) : x⁻¹ = inv x
theorem modulus_pos : 0 < modulus
theorem modulus_sq_lt_two_pow_64 : modulus ^ 2 < 2 ^ 64
theorem mul_def (x y : FastField modulus) : x * y = mul x y
theorem neg_def (x : FastField modulus) : -x = neg x
theorem ofField_toField (x : FastField modulus) : ofField (toField x) = x
theorem one_def : (1 : FastField modulus) = one modulus
theorem r2ModModulus_lt_modulus : (2 ^ 32) ^ 2 % modulus < modulus
theorem ringEquiv_apply {x : FastField modulus} : ringEquiv modulus x = toField x
theorem ringEquiv_symm_apply {x : ZMod modulus} :
theorem square_def (x : FastField modulus) : square x = x * x
theorem sub_def (x y : FastField modulus) : x - y = sub x y
theorem toField_add (x y : FastField modulus) : toField (x + y) = toField x + toField y
theorem toField_div (x y : FastField modulus) : toField (x / y) = toField x / toField y
theorem toField_injective : Function.Injective (toField (modulus
theorem toField_intCast (n : Int) : toField (n : FastField modulus) = (n : ZMod modulus)
theorem toField_inv (x : FastField modulus) : toField x⁻¹ = (toField x)⁻¹
theorem toField_mul (x y : FastField modulus) : toField (x * y) = toField x * toField y
theorem toField_natCast (n : ℕ) : toField (n : FastField modulus) = (n : ZMod modulus)
theorem toField_neg (x : FastField modulus) : toField (-x) = -toField x
theorem toField_nnqsmul (q : ℚ≥0) (x : FastField modulus) : toField (q • x) = q • toField x
theorem toField_nnratCast (q : ℚ≥0) : toField (q : FastField modulus) = (q : ZMod modulus)
theorem toField_npow (x : FastField modulus) (n : ℕ) : toField (x ^ n) = toField x ^ n
theorem toField_nsmul (n : ℕ) (x : FastField modulus) : toField (n • x) = n • toField x
theorem toField_ofCanonicalNat {n : ℕ} (h : n < modulus) :
theorem toField_ofField (x : ZMod modulus) : toField (ofField x) = x
theorem toField_one : toField (1 : FastField modulus) = 1
theorem toField_pow (x : FastField modulus) (n : ℕ) : toField (pow x n) = toField x ^ n
theorem toField_qsmul (q : ℚ) (x : FastField modulus) : toField (q • x) = q • toField x
theorem toField_ratCast (q : ℚ) : toField (q : FastField modulus) = (q : ZMod modulus)
theorem toField_square (x : FastField modulus) : toField (square x) = toField x * toField x
theorem toField_sub (x y : FastField modulus) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : FastField modulus) = 0
theorem toField_zpow (x : FastField modulus) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : FastField modulus) : toField (n • x) = n • toField x
theorem toNat_lt_modulus {x : FastField modulus} : toNat x < modulus
theorem toNat_ofCanonicalNat {n : ℕ} (h : n < modulus) :
theorem two_ne_zero : (2 : ZMod modulus) ≠ 0
theorem two_pow_32_ne_zero : ((2 ^ 32 : ℕ) : ZMod modulus) ≠ 0
theorem zero_def : (0 : FastField modulus) = zero modulus

CompPoly/Fields/Montgomery/Native64x8.lean (44)

private theorem carry_top_zero {S A B Q c : ℕ} (h : S + 2 ^ 256 * c = A + B)
private theorem cond_eq_mod {T Q : ℕ} (h : T < 2 * Q) :
private theorem cond_of_borrow_one {M Q T : ℕ} (h : M + Q = T + 2 ^ 256) (hM : M < 2 ^ 256) :
private theorem cond_of_borrow_zero {M Q T : ℕ} (h : M + Q = T) (hM : M < 2 ^ 256) :
private theorem land_mask32 (x : ℕ) : x &&& 4294967295 = x % 4294967296
private theorem sub_of_borrow_one {A B Q D E c : ℕ} (hD : D + B = A + 2 ^ 256 * 1)
private theorem sub_of_borrow_zero {A B Q D : ℕ} (h : D + B = A + 2 ^ 256 * 0)
private theorem toNat_zero : (0 : UInt64).toNat = 0
theorem Limbs8.ext_of_toNat {x y : Limbs8} (hx : x.Bounded) (hy : y.Bounded)
theorem Limbs8.toNat_lt {x : Limbs8} (hx : x.Bounded) : x.toNat < 2 ^ 256
theorem adcLo_lt (x y c : UInt64) : (adcLo x y c).toNat < 2 ^ 32
theorem adc_spec (x y c : UInt64) (hx : x.toNat < 2 ^ 32) (hy : y.toNat < 2 ^ 32)
theorem adc_spec_wide (x y c : UInt64) (hx : x.toNat < 2 ^ 33) (hy : y.toNat < 2 ^ 32)
theorem addLimbs_bounded (a b : Limbs8) : (addLimbs a b).Bounded
theorem addLimbs_toNat (a b : Limbs8) (ha : a.Bounded) (hb : b.Bounded) :
theorem add_bounded (q a b : Limbs8) : (add q a b).Bounded
theorem add_lt (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
theorem add_toNat (q a b : Limbs8) (hq : q.Bounded) (ha : a.Bounded) (hb : b.Bounded)
theorem borrow_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
theorem carry_chain_sum {x0 x1 x2 x3 x4 x5 x6 x7 y0 y1 y2 y3 y4 y5 y6 y7 : ℕ}
theorem condSub_bounded (q t : Limbs8) (ht : t.Bounded) : (condSub q t).Bounded
theorem condSub_lt (q t : Limbs8) (hq : q.Bounded) (ht : t.Bounded)

…and 170 more not listed.

✏️ Affected: 2 declaration(s) (line number changed)

abbrev Field : Type in CompPoly/Fields/KoalaBear/Fast.lean moved from L42 to L35
def ringEquiv : Field ≃+* KoalaBear.Field in CompPoly/Fields/KoalaBear/Fast.lean moved from L1003 to L52

sorry Tracking

No sorrys were added, removed, or affected.

📄 **Per-File Summaries**

CompPoly.lean: This change adds import statements for three sets of field-related submodules: CompPoly.Fields.BabyBear.Basic and Fast; a suite of CompPoly.Fields.Montgomery files (Basic, Native32, Native32Field, Native64x8, Native64x8Defs, Native64x8Field, Native64x8Mul, ScalarFft); and CompPoly.Fields.Pasta.Basic and Fast. These new imports expose additional field arithmetic implementations and supporting definitions for use throughout the CompPoly library.
CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean: The change modifies how frobenius_fixed is proved in fastKoalaBearFiniteFieldContext. Instead of using KoalaBear.Fast.toField_injective and KoalaBear.Fast.toField_npow, it now uses Montgomery.Native32.toField_injective and Montgomery.Native32.toField_npow, and simplifies the simpa by dropping the call to ZMod.pow_card. Furthermore, the proof of fastKoalaBearPrimitiveRoot_order is updated: it replaces KoalaBear.Fast.ringEquiv_apply and KoalaBear.Fast.toField_ofField with KoalaBear.Fast.ringEquiv and KoalaBear.Fast.ofField in the simpa.
CompPoly/Fields/BabyBear.lean: This file was completely rewritten from a standalone definition of the BabyBear field (with its own modulus, prime proof, two-adic generator table, and root-of-unity lemmas) into a thin facade module that re-exports the canonical ZMod model from CompPoly.Fields.BabyBear.Basic and a native-word implementation from CompPoly.Fields.BabyBear.Fast. All previously defined content — including the field size, primality theorem, precomputed two-adic generators, and lemmas about their order and primitivity — has been removed; the new module no longer defines any field structure or root-of-unity properties itself.
CompPoly/Fields/BabyBear/Basic.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file defines th...oAdicGenerators_order`.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
CompPoly/Fields/BabyBear/Fast.lean: This new file provides a fast Montgomery-arithmetic implementation of the BabyBear field using 32-bit native words. It defines an instMont32Field instance of Mont32Field for BabyBear.fieldSize with the concrete BabyBear constants (modulus32, modulus64, rModModulus, r2ModModulus, montgomeryNegInv), an abbreviation Field for the carrier type FastField BabyBear.fieldSize, and two conversion functions (ofUInt32 from UInt32, ofField from the canonical BabyBear.Field). It also supplies a ringEquiv that establishes a ring isomorphism between the fast Montgomery representation and the canonical BabyBear.Field.
CompPoly/Fields/KoalaBear/Basic.lean: The diff removes two set_option maxRecDepth pragmas (previously set to 4096 and 100000) from the file. It also simplifies both the statement and proof of primitiveRoot_pow_127_eq_twoAdicGenerator: the index is now given directly as twoAdicity instead of a cast Fin (twoAdicity+1) via ⟨twoAdicity, by omega⟩, and the proof is rewritten using norm_num followed by rfl in place of unfold primitiveRoot twoAdicity; decide.
CompPoly/Fields/KoalaBear/Fast.lean: This file was rewritten to delegate all fast KoalaBear field arithmetic to the shared CompPoly/Fields/Montgomery.Native32Field library. The old custom constants (modulus, rModModulus, etc.), private correctness lemmas, and hand-written add/mul/inv operations are replaced by a single instMont32Field instance that supplies the KoalaBear prime’s parameters. The carrier type is now FastField KoalaBear.fieldSize (an abbreviation from the shared library), and conversions (ofUInt32, ofField) delegate to the shared API. The ring equivalence ringEquiv is obtained from Montgomery.Native32.ringEquiv. Additionally, a new section adds twoAdicGenerators, a List Field of precomputed Montgomery two-adic roots, together with the theorem twoAdicGenerators_eq_map showing they match the canonical generators under ofField.
CompPoly/Fields/Montgomery/Basic.lean: This diff adds a new file CompPoly/Fields/Montgomery/Basic.lean, which introduces the Montgomery namespace and defines two core functions (reduceNat and reduceNatQuotient) for natural-number Montgomery reduction, along with five supporting lemmas. The lemma reduceNatQuotient_lt_two_mul bounds the pre-subtraction quotient below 2*p, reduceNat_lt proves the final result is below the modulus p, dvd_add establishes the key divisibility R ∣ x + ((x%R * negInv)%R) * p under the hypothesis negInv * p % R = R-1, and reduceNatQuotient_cast/reduceNat_cast show that both the quotient and the final reduced value correspond to (x : ZMod p) * (R : ZMod p)⁻¹. A final lemma natCast_inj_of_lt provides an injectivity result for Nat.cast into ZMod p for values below p. No sorry or admit are present.
CompPoly/Fields/Montgomery/Native32.lean: This file introduces CompPoly/Fields/Montgomery/Native32.lean, a new module providing raw 32-bit word-level operations for Montgomery reduction, using a radix of 2^32 and lowering to UInt32 and UInt64. It defines the core functions reduceRaw, reduceQuotient, and conditionalSubtract, along with a series of theorems (reduceRaw_eq_conditionalSubtract, reduceQuotient_toNat, conditionalSubtract_toNat, reduceRaw_toNat, conditionalSubtract_lt, conditionalSubtract_cast, reduceRaw_lt, and reduceRaw_cast) that prove these functions agree with the existing Nat-level specification in Montgomery.Basic (e.g., reduceNatQuotient, reduceNat, reduceNat_lt, reduceNat_cast). The final theorem reduceRaw_cast additionally shows that reduceRaw correctly computes the multiplication by the inverse of the radix in ZMod modulus under the standard Montgomery conditions, given Fact (Nat.Prime modulus) and a suitable negInv. The file contains no sorry or admit statements.
CompPoly/Fields/Montgomery/Native32Field.lean: Summary unavailable — error: Model 'deepseek/deepseek-v4-flash' returned no parseable structured output (finish_reason=error)
CompPoly/Fields/Montgomery/Native64x8.lean: This new file provides the correctness proofs for Montgomery arithmetic over eight 32-bit limbs (Limbs8), the multi-limb sibling of Native32.lean. It states and proves the toNat specifications for every raw word helper: adc_spec, adc_spec_wide, sbb_spec, mac_spec, and montM_toNat give existential or equational characterizations of the carry/borrow/multiply-accumulate helpers; adcLo_lt, sbbLo_lt, macLo_lt, montM_lt give bound lemmas. For the limb vector itself, it proves Limbs8.zero_bounded, Limbs8.zero_toNat, Limbs8.one_bounded, Limbs8.one_toNat, Limbs8.ofNat_bounded, Limbs8.ofNat_toNat, the extensionality lemma Limbs8.ext_of_toNat, and the value bound Limbs8.toNat_lt. It then proves the two telescoping chain lemmas carry_chain_sum and borrow_chain_sum that combine eight-step carry/borrow chains into a single identity. Finally, it proves the correctness of the field operations: addLimbs_toNat and subLimbs_spec for the underlying carry/borrow chains, and then condSub_toNat, add_toNat, sub_toNat, neg_toNat (with companion bound lemmas) for conditional subtraction, modular addition, modular subtraction, and modular negation on Limbs8, all under the assumption that 2 * q.toNat < 2^256 (i.e., the modulus is below 2^255).
CompPoly/Fields/Montgomery/Native64x8Defs.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='This new file provides z... that imports this one.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
CompPoly/Fields/Montgomery/Native64x8Field.lean: This new file defines a fast eight-limb Montgomery field for prime moduli below 2^255, serving as the multi-limb analogue of Native32Field. It introduces the Mont64x8Field typeclass (containing per-field constants such as modulusLimbs, rModModulus, r2ModModulus, and montgomeryNegInv, with side conditions discharged by decide), the FastField carrier (a subtype of Limbs8 with a boundedness and a < modulus proof), and its arithmetic (add, sub, neg, mul, square, pow, inv, div) built on the raw operations from Native64x8Mul. It provides conversion functions (toLimbs8, toNat, toField, ofCanonicalNat, ofNat, ofField), a suite of @[simp] correctness theorems (e.g., toField_add, toField_mul, toField_inv, toField_pow, toField_natCast) establishing that toField is a ring homomorphism, and the ringEquiv FastField modulus ≃+* ZMod modulus together with the transferred instField and instNonBinaryField instances.
CompPoly/Fields/Montgomery/Native64x8Mul.lean: Added the file CompPoly/Fields/Montgomery/Native64x8Mul.lean containing a correctness proof for eight-limb CIOS Montgomery multiplication. New theorems include: sum8_mul and mul_sum8 distributing scalar multiplication over limb recomposition; Limbs8.toNat_mod extracting the low limb; State9.zero_bounded, State9.zero_toNat, and State9.toNat_eq for the accumulator; mulAccum_spec stating that mulAccum exactly adds a * bi to the accumulator while preserving limb bounds; mulReduce_spec stating that mulReduce adds a multiple of the modulus to cancel the low limb and that division by 2^32 is exact; mulRound_spec giving the round invariant, bound below 2*q, and an existence claim; and mul_spec asserting that mul is canonical and satisfies 2 ^ 256 * ⟦mul a b⟧ ≡ ⟦a⟧ * ⟦b⟧ [MOD q]. Several private helper lemmas (montM_low_zero, round_bound, accum_assemble, reduce_assemble, fold8, mul_finish) support the main proofs.
CompPoly/Fields/Montgomery/ScalarFft.lean: Adds CompPoly/Fields/Montgomery/ScalarFft.lean, which defines two runtime-only functions for a radix-2 decimation-in-time FFT over eight-limb Montgomery residues: bitreverse (n l : Nat) : Nat (bit-reversal permutation index) and fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8) (logN : Nat) : Array Limbs8 (in-place FFT using the add, sub, mul primitives from Native64x8). The file deliberately imports only CompPoly.Fields.Montgomery.Native64x8Defs (itself zero-import) to keep the precompileModules closure small; no sorry or admit appear.
CompPoly/Fields/Pasta.lean: Created a new facade module CompPoly/Fields/Pasta.lean that re-exports the Pasta (Pallas/Vesta) base field implementations from CompPoly.Fields.Pasta.Basic and CompPoly.Fields.Pasta.Fast, providing a single import point for both the canonical ZMod models with primality certificates and the native-word eight-limb Montgomery representations.
CompPoly/Fields/Pasta/Basic.lean: This new file CompPoly/Fields/Pasta/Basic.lean defines the two 255-bit primes underlying the Pallas and Vesta curves and provides their primality certificates. It introduces Pallas.baseFieldSize and Vesta.baseFieldSize as Nat constants (each equal to 1 mod 2^32 with 2-adicity 32), and uses the PrattCertificate' API from CompPoly.Fields.PrattCertificate to provide Pallas.baseFieldSize_is_prime and Vesta.baseFieldSize_is_prime along with Fact instances, enabling the Field instance for each ZMod base field (Pallas.BaseField and Vesta.BaseField, both defined as abbrevs). The file also defines Pallas.scalarFieldSize as Vesta.baseFieldSize, Vesta.scalarFieldSize as Pallas.baseFieldSize, and corresponding ScalarField abbreviations that alias the other curve's base field, establishing the 2-cycle relationship. No sorry or admit is present.
CompPoly/Fields/Pasta/Fast.lean: This new file adds fast, native-word Montgomery implementations for the Pallas and Vesta base fields (the Pasta curves) using CompPoly.Fields.Montgomery.Native64x8Field. For each (Pallas.Fast and Vesta.Fast) it provides: an instMont64x8Field instance with the eight‑limb modulus, R, R², and the Montgomery inverse constant (montgomeryNegInv = 0xffffffff); the carrier type Field (an abbreviation of FastField); conversion functions ofField, toField, toNat; a ringEquiv showing the structure is equivalent to the canonical BaseField; and the two simp theorems toField_ofField / ofField_toField. No sorry or admit are present.
CompPoly/Fields/README.md: The README was reorganized to document a new Montgomery subdirectory containing generic radix reduction (Montgomery/Basic.lean), raw UInt32/UInt64 word-level operations (Montgomery/Native32.lean), a shared FastField carrier and canonical-field bridge for 32-bit moduli (Montgomery/Native32Field.lean), eight-limb Montgomery word operations for moduli below 2^255 (Montgomery/Native64x8.lean), correctness of eight-limb CIOS multiplication (Montgomery/Native64x8Mul.lean), and the per-field bounded carrier and bridge for 255-bit moduli (Montgomery/Native64x8Field.lean). A new Pasta facade (Pasta.lean) re-exports the Pallas/Vesta base fields, detailed in Pasta/Basic.lean with Pratt primality certificates, and their fast implementations in Pasta/Fast.lean as wrappers over Montgomery/Native64x8Field.lean. BabyBear and KoalaBear were split into submodules: BabyBear/Basic.lean and BabyBear/Fast.lean (and similarly for KoalaBear), with the fast modules now described as namespaced APIs forwarding Montgomery/Native32Field.lean operations and providing @[simp] equivalence lemmas. The entries for BabyBear.lean and KoalaBear.lean were updated to describe them as facades.
CompPoly/Univariate/NTT/Domain.lean: This change removes the natCast_ne_zero field from the Domain structure (which was a proof obligation that (2^logN : R) ≠ 0) and promotes it to a standalone theorem natCast_ne_zero in the Domain namespace. The Domain.inverse definition is simplified by deleting its corresponding natCast_ne_zero argument. The new theorem leverages the existing primitive witness, IsPrimitiveRoot, to derive the nonzeroness using D.primitive.neZero'.out, thereby eliminating the redundant bookkeeping field and making the Domain structure leaner.
CompPoly/Univariate/NTT/KoalaBear.lean: This diff removes two theorems and adds significant refactoring to the KoalaBear NTT domain definitions. Specifically, the file deletes twoPowNatCast_ne_zero and fast_twoPowNatCast_ne_zero (along with fast_isPrimitiveRoot_twoAdicGenerator), and eliminates the natCast_ne_zero field from the Domain structures domainOfLogN and fastDomainOfLogN. It also changes fastDomainOfLogN.omega from KoalaBear.Fast.ofField KoalaBear.twoAdicGenerators[...] to directly KoalaBear.Fast.twoAdicGenerators[...], and rewrites the primitive proof for the fast domain to use map_of_injective on the original generator's primitive root property, now relying on an equality KoalaBear.Fast.twoAdicGenerators_eq_map rather than the removed helper lemma.
bench/CompPolyBench/Common.lean: In checksumKoalaBearFast, the explicit call KoalaBear.Fast.toNat x was replaced with the method-style x.toNat. This is a syntactic refactor that does not change the function's behavior but improves consistency with other similar conversions in the file.
bench/CompPolyBench/Univariate/Common.lean: The diff removes the locally-defined ring equivalence koalaBearFastRingEquiv, the theorems koalaBearFast_isPrimitiveRoot_twoAdicGenerator and koalaBearFast_twoPowNatCast_ne_zero, and the NTT domain definition koalaBearFastDomainOfLogN. It then refactors koalaBearFastMulNttDomain and koalaBearFastBestDomainForLength? to use the corresponding centralized definitions CPolynomial.NTT.KoalaBear.fastDomainOfLogN and CPolynomial.NTT.KoalaBear.fastBestDomainForLength? respectively. This eliminates duplicate code and consolidates fast KoalaBear NTT support into the shared CPolynomial.NTT.KoalaBear module.
bench/CompPolyBench/Univariate/NTT/FastMul.lean: This pull request refactors the KoalaBear univariate multiplication benchmark. Key changes include: adding a private BenchField structure (with id and checksum fields) to encapsulate a benchmark field; renaming local variables (e.g., koalaBearMulNttFastPlan to canonicalPlan, and each benchmark record from koalaBearMul... to the more generic canonicalNtt/fastNtt); introducing canonicalField and fastField values of type BenchField for the canonical and fast fields, and computing canonicalChecksum/fastChecksum via checksumCPolynomial. All benchmark registrations (runTimed calls) were updated to use these new variable names and the BenchField.id and checksum references. This change standardizes the benchmark structure and prepares for potential extraction of field-specific configuration. No sorry or admit were introduced.
docs/wiki/binary-fields-and-ntt.md: This documentation file (docs/wiki/binary-fields-and-ntt.md) has been updated to reflect the restructuring of the project's directory layout under CompPoly/Fields/. New subdirectories and files have been added to the tree diagram: for BabyBear/Fast/ and KoalaBear/Fast/, the files Prelude.lean, Montgomery.lean, and Convert.lean are now listed; additionally, a new top-level Montgomery/ directory has been introduced, containing Basic.lean, Native32.lean, and Native32Field.lean. The Binary/ directory and its contents remain unchanged.
tests/CompPolyTests.lean: Summary unavailable — error: 1 validation error for _ProseSummary
Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The file now imports `Co... field implementations.', input_type=str]
For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
tests/CompPolyTests/Fields/BabyBear/Fast.lean: This new file (tests/CompPolyTests/Fields/BabyBear/Fast.lean) adds a test suite for the executable Montgomery representation of the BabyBear field. It imports CompPoly.Fields.BabyBear.Fast and, within the BabyBear.Fast namespace, uses a series of #guard commands to verify concrete arithmetic properties — including zero, one, addition/subtraction wraparound, negation, multiplication, exponentiation, inversion, and division — by comparing the .toNat (or .toField / .toUInt32) of results against expected values. These tests serve as regression checks ensuring that the fast field implementation behaves identically to the reference BabyBear.Field across a range of operations.
tests/CompPolyTests/Fields/KoalaBear/Fast.lean: This diff updates the #guard regression checks in tests/CompPolyTests/Fields/KoalaBear/Fast.lean to use the new explicit .val, .toUInt32, .toNat, and .toField accessor methods instead of the previous raw, toCanonicalUInt32, toNat, and toField top-level functions. The check for the representation of 1 : Field now directly references Montgomery.Native32.Mont32Field.rModModulus with an explicit modulus := binder for KoalaBear.fieldSize. The squaring test is also simplified from square (12345 : Field) to (12345 : Field) * 12345. These changes reflect a refactor of the low-level field API to use field projections and remove the earlier standalone helper functions.
tests/CompPolyTests/Fields/Montgomery/Native64x8.lean: This file adds regression tests for the eight-limb Montgomery arithmetic operations (Limbs8) for both the Vesta and Pallas base fields. It defines constants for the modulus (q, pq), the Montgomery negative inverse (negInv, pNegInv), the Montgomery radix (rMod), and sample limbs (a, b, montA, montB, montAB, pMontA, pMontB, pMontAB). The #guard statements verify that core operations—condSub, add, sub, neg, mul, and square—produce expected results (e.g., mul q negInv montA montB = montAB). It also tests the field arithmetic via the carrier types F (Vesta.Fast.Field) and G (Pallas.Fast.Field) and confirms that the canonical bridge functions Vesta.Fast.toField, Vesta.Fast.ofField, Pallas.Fast.toField, and Pallas.Fast.ofField align with ZMod arithmetic.
1 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Univariate/NTT/BabyBear.lean

Last updated: 2026-07-26 07:01 UTC.

dhsorens · 2026-09-02T14:58:42Z

hey @mitschabaude - just checking if this is ready for a review?

mitschabaude · 2026-09-02T15:13:33Z

@graikos can you fix conflicts to make review easier?

mitschabaude · 2026-09-02T15:15:12Z

ah wait no this was superseded by #284
@dhsorens

well, everything except the Pasta fields. I'll fix this to add those!

dhsorens · 2026-09-02T15:16:25Z

awesome, thanks @mitschabaude !

github-actions · 2026-09-02T15:34:20Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)

This PR adds the Pasta field instantiation and a scalar FFT module, building on the existing eight-limb Montgomery arithmetic. The new contributions are: primality certificates for the two 255-bit Pasta primes, fast Montgomery field instances for Pallas and Vesta, a zero-import runtime FFT over Montgomery residues, and the corresponding import, test, and documentation updates.

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	521
❌ Lines Removed	0

Lean Declarations

✏️ Added: 27 declaration(s)

CompPoly/Fields/Montgomery/ScalarFft.lean (2)

def bitreverse (n l : Nat) : Nat
def fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8)

CompPoly/Fields/Pasta/Basic.lean (5)

abbrev BaseField
abbrev ScalarField
abbrev scalarFieldSize : Nat
def baseFieldSize : Nat
theorem baseFieldSize_is_prime : Nat.Prime baseFieldSize

CompPoly/Fields/Pasta/Fast.lean (4)

abbrev Field : Type
def ofField (x : Vesta.BaseField) : Field
def ringEquiv : Field ≃+* Vesta.BaseField
instance instMont64x8Field : Mont64x8Field Vesta.baseFieldSize where

tests/CompPolyTests/Fields/Pasta/Fast.lean (16)

private abbrev F
private abbrev G
private def a : Limbs8
private def b : Limbs8
private def modulus : ℕ
private def montA : Limbs8
private def montAB : Limbs8
private def montB : Limbs8
private def negInv : UInt64
private def pMontA : Limbs8
private def pMontAB : Limbs8
private def pMontB : Limbs8
private def pNegInv : UInt64
private def pq : Limbs8
private def q : Limbs8
private def rMod : Limbs8

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff adds Pasta (Pallas/Vesta) fields, a scalar FFT implementation, and tests. A few minor violations of the CompPoly style guide were identified, predominantly in the test file.

📄 **Per-File Summaries**

CompPoly.lean: The diff adds three new public import statements: CompPoly.Fields.Montgomery.ScalarFft, CompPoly.Fields.Pasta, and CompPoly.Fields.Pasta.Basic (the last of which appears twice in the diff, likely a typo importing the same module twice; the intended second import is probably CompPoly.Fields.Pasta.Fast, which is also included). These imports expose implementations for a Montgomery scalar FFT and a Pasta field (with basic and fast variants), extending the project's arithmetic and field support. No new theorems, definitions, or sorries are introduced.
CompPoly/Fields/Montgomery/ScalarFft.lean: This new file CompPoly/Fields/Montgomery/ScalarFft.lean introduces the module Montgomery.ScalarFft within the Montgomery namespace, providing two runtime definitions for an in-place radix-2 decimation-in-time FFT over eight-limb Montgomery residues (Limbs8). It defines bitreverse (n l : Nat) : Nat, which computes the bit-reversal permutation index of n over l bits, and fft (q : Limbs8) (negInv : UInt64) (a0 : Array Limbs8) (tw : Array Limbs8) (logN : Nat) : Array Limbs8, which performs a bit-reversal permutation followed by logN rounds of butterflies using Montgomery arithmetic (add, sub, mul from Native64x8) against a precomputed twiddle table. The file deliberately imports nothing beyond CompPoly.Fields.Montgomery.Native64x8Defs (itself zero-import) to stay compatible with precompileModules native-compilation lanes, and contains no sorry or admit.
CompPoly/Fields/Pasta.lean: This commit adds a new file CompPoly/Fields/Pasta.lean which serves as a facade module for the Pasta fields Pallas and Vesta. It publicly re-exports the contents of two other modules: CompPoly.Fields.Pasta.Basic, which provides the canonical ZMod models with primality certificates, and CompPoly.Fields.Pasta.Fast, which provides native-word eight-limb Montgomery implementations. The module includes a docstring explaining this re-export role.
CompPoly/Fields/Pasta/Basic.lean: This new file CompPoly/Fields/Pasta/Basic.lean introduces definitions and primality proofs for the two 255-bit base prime fields of the Pallas and Vesta curves, which form a 2-cycle (the base field of one is the scalar field of the other). It defines Pallas.baseFieldSize and Vesta.baseFieldSize as reducible Nat constants, provides abbrev types Pallas.BaseField and Vesta.BaseField as the corresponding ZMod domains, and proves Pallas.baseFieldSize_is_prime and Vesta.baseFieldSize_is_prime using nested Lucas/Pratt certificates via PrattCertificate'.out. It then installs Fact (Nat.Prime baseFieldSize) instances and Field instances on the base fields. Finally, it defines reciprocal abbrevs Pallas.scalarFieldSize/Vesta.scalarFieldSize and Pallas.ScalarField/Vesta.ScalarField to reflect the cycle relationship.
CompPoly/Fields/Pasta/Fast.lean: This new file adds fast native-word Montgomery implementations for both Pasta base fields (Pallas and Vesta). It provides Mont64x8Field instances (instMont64x8Field) for each field, supplying the concrete four-limb modulus, Montgomery constants (rModModulus, r2ModModulus), and the shared montgomeryNegInv (0xffffffff). It defines the carrier abbreviation Field for each, a conversion ofField from the canonical ZMod-based Pallas.BaseField/Vesta.BaseField, and a ring equivalence ringEquiv back to the original field. The file does not contain any sorry or admit.
CompPoly/Fields/README.md: Three new files were added to the directory listing: Montgomery/ScalarFft.lean (a zero-import in-place radix-2 DIT FFT over eight-limb Montgomery residues with precomputed twiddles), Pasta.lean (a facade re-exporting the canonical Pallas/Vesta base fields and their fast native-word implementations), Pasta/Basic.lean (defining the two 255-bit Pasta base primes with Pratt primality certificates), and Pasta/Fast.lean (providing Pallas- and Vesta-namespaced APIs over the shared eight-limb fast-field implementation with per-field constants and canonical-field bridges).
tests/CompPolyTests.lean: Added a public import of CompPolyTests.Fields.Pasta.Fast, making the Pasta field's fast arithmetic implementation available for use in other modules that import this file.
tests/CompPolyTests/Fields/Pasta/Fast.lean: This new file adds regression tests for the fast Montgomery arithmetic implementations of the Pallas and Vesta fields (Pasta curves). It defines private constants and uses #guard statements to verify that low-level eight-limb operations—such as add, sub, neg, mul, square, and condSub—produce correct results against precomputed values for the Vesta field, and repeats similar checks for the Pallas field. It also tests arithmetic (addition, multiplication, exponentiation, inverse, and division) on the high-level Vesta.Fast.Field and Pallas.Fast.Field types and verifies conversion between these fast fields and the canonical BaseField representations using toField.

Last updated: 2026-09-02 15:50 UTC.

…tation Add `Fields/Pasta`, the per-field facade for the Pallas and Vesta base fields, following the KoalaBear layering: * `Pasta/Basic.lean` — the two 255-bit primes with Pratt primality certificates (ported from the certificates by Daira-Emma Hopwood, using CompPoly's own `PrattCertificate` infrastructure), their `Fact` and `Field` instances, and the 2-cycle abbreviations relating each curve's scalar field to the other's base field; * `Pasta/Fast.lean` — the `Mont64x8Field` constants for both fields and the namespaced `Pallas.Fast` / `Vesta.Fast` API over the shared eight-limb implementation, with the canonical-field bridge; * `Pasta.lean` — the facade re-exporting both. `Mont64x8Field` moves from the raw layer to `Montgomery/Native64x8Field` alongside the carrier it parameterizes, mirroring `Mont32Field` in `Montgomery/Native32Field`, and now carries `prime` like its single-word counterpart, so the bridge no longer takes a separate `Fact` argument. Tests cross-check both fast fields against canonical `ZMod` arithmetic for powers and inverses. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

dhsorens · 2026-09-02T15:59:26Z

@mitschabaude just lmk when it's ready for review :)

dhsorens

great, thanks all!

mitschabaude-bot mentioned this pull request Jul 26, 2026

Fast, proven Pasta arithmetic + fixture-check speedup zcash/ironwood#111

Merged

graikos mentioned this pull request Aug 4, 2026

feat(fields): fast BN254/BLS12-381/BLS12-377 scalar fields (8x32 Montgomery) #284

Merged

mitschabaude-bot force-pushed the fast_multilimb_fields branch 2 times, most recently from bddc016 to 444947f Compare September 2, 2026 15:31

mitschabaude reviewed Sep 2, 2026

View reviewed changes

Comment thread CompPoly/Fields/Pasta/Fast.lean Outdated

Comment thread CompPoly/Fields/Pasta/Fast.lean Outdated

Comment thread CompPoly/Fields/Pasta/Fast.lean Outdated

Comment thread CompPoly/Fields/Pasta/Fast.lean Outdated

mitschabaude-bot and others added 2 commits September 2, 2026 17:48

feat(fields): scalar radix-2 FFT over eight-limb Montgomery elements

37685bc

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

mitschabaude-bot force-pushed the fast_multilimb_fields branch from 444947f to 37685bc Compare September 2, 2026 15:48

mitschabaude-bot marked this pull request as ready for review September 2, 2026 16:03

dhsorens approved these changes Sep 2, 2026

View reviewed changes

dhsorens merged commit 322f12e into Verified-zkEVM:main Sep 2, 2026
5 checks passed

Navigation Menu

Uh oh!

Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta) - #274

Eight-limb Montgomery field arithmetic for 255-bit moduli (Pasta)#274
dhsorens merged 2 commits into
Verified-zkEVM:mainfrom
mitschabaude-bot:fast_multilimb_fields

mitschabaude-bot commented Jul 25, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 25, 2026 •

edited

Loading

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

mitschabaude commented Sep 2, 2026

Uh oh!

mitschabaude commented Sep 2, 2026

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

github-actions Bot commented Sep 2, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

dhsorens left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

mitschabaude-bot commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Runtime layout

Validation

Uh oh!

github-actions Bot commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

mitschabaude commented Sep 2, 2026

Uh oh!

mitschabaude commented Sep 2, 2026

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

github-actions Bot commented Sep 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dhsorens commented Sep 2, 2026

Uh oh!

dhsorens left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mitschabaude-bot commented Jul 25, 2026 •

edited

Loading

github-actions Bot commented Jul 25, 2026 •

edited

Loading

github-actions Bot commented Sep 2, 2026 •

edited

Loading